COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "let.pub[let,jmc]" source
C00006 ENDMK
C⊗;
.require "let.pub[let,jmc]" source;
∂CSL Professor W. W. Bledsoe↓Department of Mathematics
↓University of Texas↓Austin, Texas 78712∞

Dear Woody:

	I hope to make the meeting in SF, possibly a bit late because of a
class.  Anyway I have an idea for an intermediate prize.

	The program used to verify the four-color theorem was never proved
correct - either by hand or machine.  It is disgraceful that the referees
wrote their own program.  It is almost as though a proof was offered that
consisted of a selection of cases and the referees accepted the paper on
the basis of some further examples.

	Whether one regards the above analogy as valid or not, it is clear
that assurance of the correctness of the four color conjecture would be
greater if the program had been proved to meet certain specifications.
Even suppose that no-one had proved anything aobut the programming
language, the compiler or the computer itself.  It is ultimately desirable
to prove them correct also, but there is an important distinction between
them and the program specifically intended to verify the conjecture in
that the latter is subject to wishful thinking by the author and even by
the referees.

	My suggestion then is that the committee offer a prize for the
first computer-checked proof (whether generated by computer or not) that a
program is correct that is the basis of a substantial published proof of a
matematical conjecture.

	There is a lesser example than the four color theorem which I
understand better.  A Stanford CS graduate student named Oren Patashnik,
while at Yale, proved that 3 dimensional tic-tac-toe with four on a side
is a win for the first player using about 1500 hours of computer time.
The paper about it was recently published in %2Mathematics Magazine%1.  In
my opinion, it wouldn't be very hard to prove correct a program that
verifies cases.  .next page;
	Like the four color problem, Patashniks proof involved finding
winning moves in certain situations with the help of the computer and then
using the computer to verify that the moves were winning and the positions
formed an adequate set.  I think he or someone else would deserve a
moderate prize for a computer checked proof.  More than likely, a new
program would be written for the verification work that would be easier to
prove correct and would run in a reasonable time.

.reg